Many electronic devices, such as systems-on-chips (SoCs), include hardware that implements a data transformation pipeline. As is known to those of skill in the art, a pipeline comprises a set of processing elements wherein the output of a processing element in the set is the input to a processing element in the set. A data transformation pipeline is a type of pipeline that is configured to perform a data transformation on a set of one or more inputs. The term “data transformation” is used herein to mean any operation (e.g. mathematical operations such as, but not limited to, arithmetic operations including addition, subtraction, multiplication, division etc.) that can be performed on, or applied to, a set of data to produce new data. Accordingly, a data transformation pipeline receives a set of one or more inputs and outputs the result of a data transformation performed on the set of inputs. A data transformation pipeline comprises at least one data transformation element configured to perform a data transformation on a set of inputs, but it may also include other types of processing elements. When a pipeline generates an output for a set of inputs the pipeline is said to execute a ‘transaction’. Accordingly, a pipeline is said to execute the same transaction if it generates an output for the same set of inputs.
A data transformation pipeline may be a linear or non-linear pipeline and it may have a single processing element or multiple processing elements. FIGS. 1-3 illustrate example data transformation pipelines configured to perform an arithmetic calculation on a set of inputs. FIG. 1 illustrates a first example data transformation pipeline 100 configured to calculate the sum of eight inputs (a0+a1+a2+a3+a4+a5+a6+a7). The data transformation pipeline 100 of FIG. 1 comprises a single data transformation element 102, a register 104 and control logic 106. The data transformation element 102 receives an input ai in each of eight cycles (numbered 0 to 7) and adds the input to the sum of the previous inputs bi (i.e. the value of the register 104 in the previous cycle) and stores the new sum in the register 104. The control logic 106 is configured to provide the value of the register 104 to the data transformation element 102 in each cycle, and output the value of the register 104 after the eighth cycle (i.e. after the sum a0+a1+a2+a3+a4+a5+a6+a7 has been generated). The control logic 106 is also configured to set the value of the register 104 to 0 on reset and after the value of the register 104 is output. Where the data transformation element 102 is configured to generate the sum of the two inputs (ai and bi) in a single cycle the output of the pipeline may be expected to be output after eight cycles. However, there may be random external events, such as stalls or interrupts, which affect the movement of data through the pipeline by one or more clock cycles.
FIG. 2 illustrates a second example data transformation pipeline 200 configured to calculate (a+b)*c. The data transformation pipeline 200 comprises two data transformation elements 202, 204, a register 206, and control logic 208. The first data transformation element 202 is configured to calculate the sum of the inputs a and b and store the sum y in the register 206. The second data transformation element 204 is configured to calculate the product of the register 206 value (i.e. the output of the first data transformation element 202 y) and the input c. The control logic 208 controls the operation of the register 206 to ensure that the value of the register 206 is provided to the second data transformation element 204 at the correct time.
FIG. 3 illustrates a third example data transformation pipeline 300 configured to calculate (a+b). The data transformation pipeline 300 comprises two processing elements 302, 304, a register 306 and control logic 308. The first processing element 302 is a data transformation element configured to calculate the sum of the inputs a and b. The second processing element 304 is not a data transformation element as it does not transform the data input thereto, it simply stores the value of the register 306 (i.e. the output of the data transformation element 302) y until the result is requested by a downstream component. The control logic 308 controls the operation of the register 306 to ensure that the value of the register 306 is provided to the second processing element 304 at the correct time.
Generating hardware that implements a data transformation pipeline typically includes developing a hardware design that describes the structure and/or function of an integrated circuit that implements the data transformation pipeline; verifying or testing the hardware design to ensure that an integrated circuit manufactured according to the design will behave as expected; and once verified, manufacturing an integrated circuit, at an integrated circuit manufacturing system, in accordance with the hardware design.
In some cases, verifying the hardware design for a data transformation pipeline may comprise verifying that an instantiation of the hardware design produces the correct result to the data transformation regardless of when the transformation is performed. Specifically, since a data transformation pipeline may perform a transformation at any time after reset (e.g. immediately after reset, or, for example, 10,000 cycles after reset) and with a variable amount of latency (e.g. due to stalls or interrupts) it is important to verify that regardless of when the transformation is performed that an instantiation of the hardware design will produce the correct result to the transformation.
In other cases, verifying the hardware design for a data transformation pipeline may comprise verifying that an instantiation of the hardware design always (regardless of when the transformation is performed) produces the same result as an instantiation of another similar hardware design. This type of verification may be referred to as verifying that the hardware designs are functionally equivalent. This type of verification may be used when an original hardware design is modified to verify that the modified hardware design will produce the same results as the original hardware design.
A hardware design may be verified, for example, by formal verification or simulation-based verification. Formal verification is a systematic process that uses a mathematical model of the hardware design and mathematical reasoning to verify the hardware design. In contrast, simulation-based verification is a process in which a hardware design is tested by applying stimuli to an instantiation of the hardware design and monitoring the output of the instantiation of the hardware design in response to the stimuli.
In formal verification, the hardware design is transformed into a mathematical model (e.g. a state-transition system, or a flow graph) to thereby provide an instantiation of the hardware design which can be tested to verify the hardware design, and formal properties to be verified are expressed using mathematical logic using a precise syntax or a language with a precise mathematical syntax and semantics.
Formal verification is performed using a formal verification tool (i.e. a software tool that is capable of performing formal verification of a hardware design). Formal verification tools include, but are not limited to, formal equivalence checkers such as OneSpin 360 DV™, Mentor Graphics Questa® Formal Verification, Synopsys® VC Formal, Cadence® Incisive® Enterprise Verifier, and JasperGold®; and formal property checkers (which may also be referred to as formal model checkers) such as Synopsys® HECTOR, and other logical equivalence checkers (LECs) and sequential logical equivalence checkers (SLECs)). Some formal verification tools, which may be referred to herein as arithmetic formal verification tools, are proficient at verifying properties related to data transformations (such as arithmetic operations) but can typically only be used to prove a property over a finite period of time. Other verification tools, which may be referred to herein as infinite time formal verification tools are proficient at verifying a property over an infinite time period but are poor at verifying properties related to data transformations (such as arithmetic operations).
Since existing formal verification tools are proficient at verifying properties related to data transformations, or proficient at verifying a property over infinite time, not both, it is difficult, if not impossible, using an existing formal verification tool to verify the output of an instantiation of a hardware design for a data transformation over infinite time. Accordingly it is difficult, using an existing formal verification tool to verify that an instantiation of a hardware design for a data transformation pipeline will always transform the data correctly, or will always transform the data in the same manner as an instantiation of another hardware design, regardless of when the transformation is performed.
The embodiments described below are provided by way of example only and are not limiting of implementations which solve any or all of the disadvantages of known methods and systems for verifying a hardware design for a data transformation pipeline.